Refine yourself a code for great good!

Abstract: How do you code? Andrej Karpathy who coined the term "vibe coding," says that for professional coding tasks, he picks single concrete incremental changes and, with AI assistance, plans them, executes them, and evaluates them. Refinement is the process of making incremental changes. It is not just the primary way we design and construct code, but also how we repair them and upgrade them, often collaboratively with other coders, designers and users.

The central objects in refinement are partially implemented programs. Partial programs are examples of open systems - each has a formal external specification (e.g. a function type) and an implementation with internal holes which are also formally specified. Partial proofs, such as those manipulated by the proof assistants, are also examples of open systems. Open systems compose by refinement or hole-filling, where a typed hole can only be filled by an open system of the right spec. An open system in some representation can also be translated (transported, projected or lifted) to some open system in another representation. In fact, open systems, with their refinements and translations, form a double category!

In this talk, I hope to share some concrete examples of this refinement-centric approach in formal verification, program synthesis and theorem proving. I believe that this approach can help us to leverage AI assistance in coding, to decentralize and democratize coding, and to build safe, secure and sustainable software systems.

Moderator: The talk will be moderated by Daniel Filonik. Daniel specializes in data visualization and human computer interaction. His recent work focused on natural interfaces for interactive data modeling and analysis with formal foundations in category theory.

Computer scienceMathematics

Audience: researchers in the topic

( video )

---

Relatorium seminar

Series comments: The name "Relatorium" combines "relator" with the Latin root "-ium," meaning "a place for activities" (as in "auditorium" or "gymnasium"). This seminar series is a platform to relate ideas, interact with math, and connect with each other.

In this series, we explore math beyond what we usually hear in standard talks. These sessions fall somewhere between a technical talk and a podcast: moderately formal, yet conversational. The philosophy behind the series is that math is best learned by active participation rather than passive listening. Our aim is to “engage and involve,” inviting everyone to think actively with the speaker. The concepts are accessible, exploratory, and intended to spark questions and discussions.

The idea of relatability has strong ties to compassion — creating space for shared understanding and exploration - which is the spirit of this seminar! This is a pilot project, so we’re here to improvise, learn, and evolve as we go!

---